
Load RCC axioms and inverses

Show lemma1
=============================
Step 1

? (all x (all y ((pp x y) => ((tpp x y) v (ntpp x y)))))


> revsk
=============================
Step 2

? ((~ (pp c177290 c177289)) v ((tpp c177290 c177289) v (ntpp c177290 c177289)))


> hypdisj
=============================
Step 3

? (ntpp c177290 c177289)

1. (~ (tpp c177290 c177289))
2. (pp c177290 c177289)

> ((ntpp Z X) <-- (pp Z X) (~ (ec (f172288 Z X Y) Z)))
|=============================
|Step 4
|
|? (pp c177290 c177289)
|
|1. (~ (ntpp c177290 c177289))
|2. (~ (tpp c177290 c177289))
|3. (pp c177290 c177289)
|
|> hyp
=============================
Step 5

? (~ (ec (f172288 c177290 c177289 Var32) c177290))

1. (~ (ntpp c177290 c177289))
2. (~ (tpp c177290 c177289))
3. (pp c177290 c177289)

> ((~ (ec X Y)) <-- (pp Y Z) (ec X Z) (~ (tpp Y Z)))
||=============================
||Step 6
||
||? (pp c177290 Var36)
||
||1. (ec (f172288 c177290 c177289 Var32) c177290)
||2. (~ (ntpp c177290 c177289))
||3. (~ (tpp c177290 c177289))
||4. (pp c177290 c177289)
||
||> hyp
|=============================
|Step 7
|
|? (ec (f172288 c177290 c177289 Var32) c177289)
|
|1. (ec (f172288 c177290 c177289 Var32) c177290)
|2. (~ (ntpp c177290 c177289))
|3. (~ (tpp c177290 c177289))
|4. (pp c177290 c177289)
|
|> ((ec (f172288 Y Z X) Z) <-- (~ (ntpp Y Z)) (pp Y Z))
||=============================
||Step 8
||
||? (~ (ntpp c177290 c177289))
||
||1. (~ (ec (f172288 c177290 c177289 Var32) c177289))
||2. (ec (f172288 c177290 c177289 Var32) c177290)
||3. (~ (ntpp c177290 c177289))
||4. (~ (tpp c177290 c177289))
||5. (pp c177290 c177289)
||
||> hyp
|=============================
|Step 9
|
|? (pp c177290 c177289)
|
|1. (~ (ec (f172288 c177290 c177289 Var32) c177289))
|2. (ec (f172288 c177290 c177289 Var32) c177290)
|3. (~ (ntpp c177290 c177289))
|4. (~ (tpp c177290 c177289))
|5. (pp c177290 c177289)
|
|> hyp
=============================
Step 10

? (~ (tpp c177290 c177289))

1. (ec (f172288 c177290 c177289 Var32) c177290)
2. (~ (ntpp c177290 c177289))
3. (~ (tpp c177290 c177289))
4. (pp c177290 c177289)

> hyp

Finally prove main theorem

=============================
Step 1

? (all x (all y (all z (((dc x y) & (ec y z)) => (((((dc x z) v (ec x z)) v (po x z)) v (tpp x z)) v (ntpp x z))))))


> revsk
=============================
Step 2

? (((~ (dc c182516 c182515)) v (~ (ec c182515 c182514))) v (((((dc c182516 c182514) v (ec c182516 c182514)) v (po c182516 c182514)) v (tpp c182516 c182514)) v (ntpp c182516 c182514)))


> hypdisj
=============================
Step 3

? (ntpp c182516 c182514)

1. (~ (tpp c182516 c182514))
2. (~ (po c182516 c182514))
3. (~ (ec c182516 c182514))
4. (~ (dc c182516 c182514))
5. (ec c182515 c182514)
6. (dc c182516 c182515)

> ((ntpp X Y) <-- (pp X Y) (~ (tpp X Y)))
|=============================
|Step 4
|
|? (pp c182516 c182514)
|
|1. (~ (ntpp c182516 c182514))
|2. (~ (tpp c182516 c182514))
|3. (~ (po c182516 c182514))
|4. (~ (ec c182516 c182514))
|5. (~ (dc c182516 c182514))
|6. (ec c182515 c182514)
|7. (dc c182516 c182515)
|
|> ((pp Y X) <-- (p Y X) (~ (p X Y)))
||=============================
||Step 5
||
||? (p c182516 c182514)
||
||1. (~ (pp c182516 c182514))
||2. (~ (ntpp c182516 c182514))
||3. (~ (tpp c182516 c182514))
||4. (~ (po c182516 c182514))
||5. (~ (ec c182516 c182514))
||6. (~ (dc c182516 c182514))
||7. (ec c182515 c182514)
||8. (dc c182516 c182515)
||
||> ((p X Y) <-- (o X Y) (~ (p Y X)) (~ (po X Y)))
||||=============================
||||Step 6
||||
||||? (o c182516 c182514)
||||
||||1. (~ (p c182516 c182514))
||||2. (~ (pp c182516 c182514))
||||3. (~ (ntpp c182516 c182514))
||||4. (~ (tpp c182516 c182514))
||||5. (~ (po c182516 c182514))
||||6. (~ (ec c182516 c182514))
||||7. (~ (dc c182516 c182514))
||||8. (ec c182515 c182514)
||||9. (dc c182516 c182515)
||||
||||> ((o X Y) <-- (c X Y) (~ (ec X Y)))
|||||=============================
|||||Step 7
|||||
|||||? (c c182516 c182514)
|||||
|||||1. (~ (o c182516 c182514))
|||||2. (~ (p c182516 c182514))
|||||3. (~ (pp c182516 c182514))
|||||4. (~ (ntpp c182516 c182514))
|||||5. (~ (tpp c182516 c182514))
|||||6. (~ (po c182516 c182514))
|||||7. (~ (ec c182516 c182514))
|||||8. (~ (dc c182516 c182514))
|||||9. (ec c182515 c182514)
|||||10. (dc c182516 c182515)
|||||
|||||> ((c X Y) <-- (~ (dc X Y)))
|||||=============================
|||||Step 8
|||||
|||||? (~ (dc c182516 c182514))
|||||
|||||1. (~ (c c182516 c182514))
|||||2. (~ (o c182516 c182514))
|||||3. (~ (p c182516 c182514))
|||||4. (~ (pp c182516 c182514))
|||||5. (~ (ntpp c182516 c182514))
|||||6. (~ (tpp c182516 c182514))
|||||7. (~ (po c182516 c182514))
|||||8. (~ (ec c182516 c182514))
|||||9. (~ (dc c182516 c182514))
|||||10. (ec c182515 c182514)
|||||11. (dc c182516 c182515)
|||||
|||||> hyp
||||=============================
||||Step 9
||||
||||? (~ (ec c182516 c182514))
||||
||||1. (~ (o c182516 c182514))
||||2. (~ (p c182516 c182514))
||||3. (~ (pp c182516 c182514))
||||4. (~ (ntpp c182516 c182514))
||||5. (~ (tpp c182516 c182514))
||||6. (~ (po c182516 c182514))
||||7. (~ (ec c182516 c182514))
||||8. (~ (dc c182516 c182514))
||||9. (ec c182515 c182514)
||||10. (dc c182516 c182515)
||||
||||> hyp
|||=============================
|||Step 10
|||
|||? (~ (p c182514 c182516))
|||
|||1. (~ (p c182516 c182514))
|||2. (~ (pp c182516 c182514))
|||3. (~ (ntpp c182516 c182514))
|||4. (~ (tpp c182516 c182514))
|||5. (~ (po c182516 c182514))
|||6. (~ (ec c182516 c182514))
|||7. (~ (dc c182516 c182514))
|||8. (ec c182515 c182514)
|||9. (dc c182516 c182515)
|||
|||> ((~ (p X Z)) <-- (c Y X) (~ (c Y Z)))
||||=============================
||||Step 11
||||
||||? (c Var67 c182514)
||||
||||1. (p c182514 c182516)
||||2. (~ (p c182516 c182514))
||||3. (~ (pp c182516 c182514))
||||4. (~ (ntpp c182516 c182514))
||||5. (~ (tpp c182516 c182514))
||||6. (~ (po c182516 c182514))
||||7. (~ (ec c182516 c182514))
||||8. (~ (dc c182516 c182514))
||||9. (ec c182515 c182514)
||||10. (dc c182516 c182515)
||||
||||> ((c X Y) <-- (ec X Y))
||||=============================
||||Step 12
||||
||||? (ec Var67 c182514)
||||
||||1. (~ (c Var67 c182514))
||||2. (p c182514 c182516)
||||3. (~ (p c182516 c182514))
||||4. (~ (pp c182516 c182514))
||||5. (~ (ntpp c182516 c182514))
||||6. (~ (tpp c182516 c182514))
||||7. (~ (po c182516 c182514))
||||8. (~ (ec c182516 c182514))
||||9. (~ (dc c182516 c182514))
||||10. (ec c182515 c182514)
||||11. (dc c182516 c182515)
||||
||||> hyp
|||=============================
|||Step 13
|||
|||? (~ (c c182515 c182516))
|||
|||1. (p c182514 c182516)
|||2. (~ (p c182516 c182514))
|||3. (~ (pp c182516 c182514))
|||4. (~ (ntpp c182516 c182514))
|||5. (~ (tpp c182516 c182514))
|||6. (~ (po c182516 c182514))
|||7. (~ (ec c182516 c182514))
|||8. (~ (dc c182516 c182514))
|||9. (ec c182515 c182514)
|||10. (dc c182516 c182515)
|||
|||> ((~ (c Y X)) <-- (~ (c X Y)))
|||=============================
|||Step 14
|||
|||? (~ (c c182516 c182515))
|||
|||1. (c c182515 c182516)
|||2. (p c182514 c182516)
|||3. (~ (p c182516 c182514))
|||4. (~ (pp c182516 c182514))
|||5. (~ (ntpp c182516 c182514))
|||6. (~ (tpp c182516 c182514))
|||7. (~ (po c182516 c182514))
|||8. (~ (ec c182516 c182514))
|||9. (~ (dc c182516 c182514))
|||10. (ec c182515 c182514)
|||11. (dc c182516 c182515)
|||
|||> ((~ (c X Y)) <-- (dc X Y))
|||=============================
|||Step 15
|||
|||? (dc c182516 c182515)
|||
|||1. (c c182516 c182515)
|||2. (c c182515 c182516)
|||3. (p c182514 c182516)
|||4. (~ (p c182516 c182514))
|||5. (~ (pp c182516 c182514))
|||6. (~ (ntpp c182516 c182514))
|||7. (~ (tpp c182516 c182514))
|||8. (~ (po c182516 c182514))
|||9. (~ (ec c182516 c182514))
|||10. (~ (dc c182516 c182514))
|||11. (ec c182515 c182514)
|||12. (dc c182516 c182515)
|||
|||> hyp
||=============================
||Step 16
||
||? (~ (po c182516 c182514))
||
||1. (~ (p c182516 c182514))
||2. (~ (pp c182516 c182514))
||3. (~ (ntpp c182516 c182514))
||4. (~ (tpp c182516 c182514))
||5. (~ (po c182516 c182514))
||6. (~ (ec c182516 c182514))
||7. (~ (dc c182516 c182514))
||8. (ec c182515 c182514)
||9. (dc c182516 c182515)
||
||> hyp
|=============================
|Step 17
|
|? (~ (p c182514 c182516))
|
|1. (~ (pp c182516 c182514))
|2. (~ (ntpp c182516 c182514))
|3. (~ (tpp c182516 c182514))
|4. (~ (po c182516 c182514))
|5. (~ (ec c182516 c182514))
|6. (~ (dc c182516 c182514))
|7. (ec c182515 c182514)
|8. (dc c182516 c182515)
|
|> ((~ (p X Z)) <-- (c Y X) (~ (c Y Z)))
||=============================
||Step 18
||
||? (c Var79 c182514)
||
||1. (p c182514 c182516)
||2. (~ (pp c182516 c182514))
||3. (~ (ntpp c182516 c182514))
||4. (~ (tpp c182516 c182514))
||5. (~ (po c182516 c182514))
||6. (~ (ec c182516 c182514))
||7. (~ (dc c182516 c182514))
||8. (ec c182515 c182514)
||9. (dc c182516 c182515)
||
||> ((c X Y) <-- (ec X Y))
||=============================
||Step 19
||
||? (ec Var79 c182514)
||
||1. (~ (c Var79 c182514))
||2. (p c182514 c182516)
||3. (~ (pp c182516 c182514))
||4. (~ (ntpp c182516 c182514))
||5. (~ (tpp c182516 c182514))
||6. (~ (po c182516 c182514))
||7. (~ (ec c182516 c182514))
||8. (~ (dc c182516 c182514))
||9. (ec c182515 c182514)
||10. (dc c182516 c182515)
||
||> hyp
|=============================
|Step 20
|
|? (~ (c c182515 c182516))
|
|1. (p c182514 c182516)
|2. (~ (pp c182516 c182514))
|3. (~ (ntpp c182516 c182514))
|4. (~ (tpp c182516 c182514))
|5. (~ (po c182516 c182514))
|6. (~ (ec c182516 c182514))
|7. (~ (dc c182516 c182514))
|8. (ec c182515 c182514)
|9. (dc c182516 c182515)
|
|> ((~ (c Y X)) <-- (~ (c X Y)))
|=============================
|Step 21
|
|? (~ (c c182516 c182515))
|
|1. (c c182515 c182516)
|2. (p c182514 c182516)
|3. (~ (pp c182516 c182514))
|4. (~ (ntpp c182516 c182514))
|5. (~ (tpp c182516 c182514))
|6. (~ (po c182516 c182514))
|7. (~ (ec c182516 c182514))
|8. (~ (dc c182516 c182514))
|9. (ec c182515 c182514)
|10. (dc c182516 c182515)
|
|> ((~ (c X Y)) <-- (dc X Y))
|=============================
|Step 22
|
|? (dc c182516 c182515)
|
|1. (c c182516 c182515)
|2. (c c182515 c182516)
|3. (p c182514 c182516)
|4. (~ (pp c182516 c182514))
|5. (~ (ntpp c182516 c182514))
|6. (~ (tpp c182516 c182514))
|7. (~ (po c182516 c182514))
|8. (~ (ec c182516 c182514))
|9. (~ (dc c182516 c182514))
|10. (ec c182515 c182514)
|11. (dc c182516 c182515)
|
|> hyp
=============================
Step 23

? (~ (tpp c182516 c182514))

1. (~ (ntpp c182516 c182514))
2. (~ (tpp c182516 c182514))
3. (~ (po c182516 c182514))
4. (~ (ec c182516 c182514))
5. (~ (dc c182516 c182514))
6. (ec c182515 c182514)
7. (dc c182516 c182515)

> hyp
